Consider the TRS R consisting of the rewrite rules
1:
app(id,x)
→ x
2:
app(plus,0)
→ id
3:
app(app(plus,app(s,x)),y)
→ app(s,app(app(plus,x),y))
There are 3 dependency pairs:
4:
APP(app(plus,app(s,x)),y)
→ APP(s,app(app(plus,x),y))
5:
APP(app(plus,app(s,x)),y)
→ APP(app(plus,x),y)
6:
APP(app(plus,app(s,x)),y)
→ APP(plus,x)
The approximated dependency graph contains one SCC:
{5}.
Consider the SCC {5}.
By taking the AF π with
π(APP) = 1 together with
the lexicographic path order with
precedence plus ≻ id,
the rules in {1-3,5}
are strictly decreasing.